E, A:Type, info:(E((:Id  A) + (:(:IdLnk  E)  Id))), e:E.
(rcv?(e))  (rtag(info;e)  Id) 

latex

Definitions	x:A. B(x), P  Q, b, rcv?(e), t  T, rtag(info;e), ecase1(e;info;i.f(i);l,e'.g(l;e')), ff, tt, t.2, if b then t else f fi , False,
Lemmas	IdLnk wf, false wf, true wf, assert wf, rcv? wf, Id wf